Inference at * 
Iof proof for Lemma primrec add:


  T:Type, n, m:, b:T, c:({0..(n+m)}TT).
  primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t)) 

latex

 by ((((RepeatFor 2 ((D 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 
C3:n)) (first_tok :t) inil_term)))) 
CollapseTHEN (NatInd (-1)))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. T : Type
C1: 2. m : 
C1: 3. b : T
C1: 4. c : {0..(0+m)}TT
C1:   primrec(0+m;b;c) = primrec(0;primrec(m;b;c);i,t. c(i+m,t))
C2: 

C2: 1. T : Type
C2: 2. n : 
C2: 3. 0 < n
C2: 4. m:, b:T, c:({0..((n - 1)+m)}TT).
C2: 4. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);i,t. c(i+m,t))
C2: 5. m : 
C2: 6. b : T
C2: 7. c : {0..(n+m)}TT
C2:   primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))
C.

Definitions	False, A, A  B, i  j , P  Q, t  T, x:A. B(x), ,
Lemmas	ge wf, nat properties, int seg wf, nat wf